\section{Conclusions}
\label{sec:conclusions}

We described our tool Zeno along with the steps it uses in constructing proofs and the heuristics we have developed for trimming the search space for these steps. Rather than pre-compute induction schemata we allow our tool to gradually build one up through multiple steps, guided by critical terms.

 Zeno is able to discover its proofs in a fully automated way, requiring no auxiliary lemmas to be suggested by the user, and indeed often discovers many interesting lemmas on its way to a larger proof.

We found that Zeno compared favourably   with the tools IsaPlanner and ACL2s
both in terms of theorem  proving power and speed, albeit within a restricted domain. 
 
%, showing that we have found a suitably general set of steps with which to construct proofs. Even though speed is not paramount in the field of theorem proving we are pleased that our tool gave good performance times as we feel this highlights the success of our heuristics in trimming the required search space.





\subsubsection{Acknowledgements} We thank Davide Ancona and the SLURP group for feedback, Tristan Alwood for lots of interesting discussions, Moa Johansson for her help with IsaPlanner, and Krysia Broda for her knowledgeable advice. 